n, m:, f, g:(nm), d:.
sum(f(x,y)-g(x,y) | x < n; y < m) = d
 sum(f(x,y) | x < n; y < m) = sum(g(x,y) | x < n; y < m)+d 

latex

Definitions	AB, A, False, P  Q, Prop, sum(f(x;y) | x < n; y < m), x,y. t(x;y), x(s1,s2), {i..j}, x:A. B(x), t  T, , sum(f(x) | x < k), x. t(x), SQType(T), {T}, i  j < k, P & Q
Lemmas	sum functionality, sum wf, sum difference, nat wf, int seg wf, double sum wf